Erasure-subtyping-1.agda:2,7-8
@0 A → B !=< A → B because one is a non-erased function type and
the other is an erased function type
when checking that the expression g has type A → B
